Nuprl Lemma : fpf-ap_wf
0,22
postcript
pdf
A
:Type,
B
:(
A
Type),
f
:
a
:
A
fp
B
(
a
),
eq
:EqDecider(
A
),
x
:
A
.
x
dom(
f
)
f
(
x
)
B
(
x
)
latex
Definitions
P
Q
,
P
&
Q
,
a
:
A
fp
B
(
a
)
,
x
dom(
f
)
,
f
(
x
)
,
P
Q
,
2of(
t
)
,
b
,
deq-member(
eq
;
x
;
L
)
,
1of(
t
)
,
x
.
t
(
x
)
,
EqDecider(
T
)
,
(
x
l
)
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
t
T
Lemmas
l
member
wf
,
deq
wf
,
pi1
wf
,
deq-member
wf
,
assert
wf
,
pi2
wf
,
assert-deq-member
origin
A:Type, B:(A
Type), f:a:A fp B(a), eq:EqDecider(A), x:A. x 
dom(f) 
f(x) B(x) A:Type, B:(AType), f:a:A fp B(a), eq:EqDecider(A), x:A. x dom(f) f(x) B(x) 
Q B(a) dom(f) Q
b
x. t(x) l)x:A. B(x) T